…6-05-03 EOD progress (#1402)

Reflects substantive progress this session across the math-proofs
honest assessment matrix. Key state changes:

**P0 items — 3 of 3 closed:**
- Lean lake-build CI job ✓ (#1394)
- A4 registry rows ✓ (#1393)
- Peer-review email draft ✓ (#1387)
- Stryker B3 → partial (config-fix #1395; CI wire deferred to
  follow-up substantial-design)

**P1 items — significant progress:**
- Alloy B2 → A ✓ (#1396 — silent-no-op was the failure mode;
  spec-path fixed)
- Semgrep B4 → A ✓ (verify-then-claim correction; was already
  in CI)
- B1 4 deferred specs → 2 of 4 done:
  - DbspSpec ✓ #1397 (1M states / 11s)
  - CircuitRegistration ✓ #1401 (B-0180 closed; 3538 states / <1s)
  - SpineAsyncProtocol B-0179 still open (counterexample inv.)
  - SpineMergeInvariants B-0181 still open (counterexample inv.)

**Sibling work tracked:**
- Phase 0 substrate-discovery PoC ✓ (#1392 — 4.0 MB AOT binary
  on osx-arm64; cross-platform CI matrix)
- 3 broken-spec backlog rows filed (#1398 → B-0179 + B-0180 +
  B-0181); B-0180 closed (#1401)
- `.ts/.sh` parity bug in `tools/backlog/generate-index.ts`
  closed ✓ (#1400 — both generators byte-identical)

This update is bounded substrate work documenting the actual
state of the matrix; doesn't add new work, just captures
completion. Future matrix re-grades happen as work-items land
(per the assessment doc's audit-trail discipline).

Composes with #1383 (the original assessment) + every PR
referenced above.

§33 archive-header lint passes.

…ster + cache-clobber discipline encoded (#1408)

Substantial multi-tick session shard. 18 PRs touched (#1383 + #1387
+ #1392-#1407 inclusive); 14 merged + 4 in-flight as of shard time.

**Math-proofs assessment progress** (#1383 outstanding-work matrix):
- A1+A2 → A-with-CI ✓ (#1394 Lean lake-build workflow)
- A4 registry rows ✓ (#1393)
- B1 → 2 of 4 deferred specs in CI ✓ (#1397 DbspSpec + #1401
  CircuitRegistration B-0180 closed)
- B2 Alloy → A ✓ (#1396 silent-no-op spec-path fix)
- B4 Semgrep → A ✓ (correction)
- Peer-review email template ✓ (#1387)
- Phase 0 substrate-discovery PoC ✓ (#1392)
- Stryker config-fix ✓ (#1395; CI wire deferred)
- 3 broken-spec backlog rows filed ✓ (#1398)

**Cache-clobber silent-bug class discovered + fully encoded:**
B-0180 fix passing locally + failing CI → verify-then-claim
identified gate.yml + low-memory.yml caching whole tools/tla and
tools/alloy directories. Fix cluster: #1403 (gate.yml) + #1404
(low-memory.yml + audit-ci-cache-paths.ts) + #1406 (CI lint gate)
+ #1407 (memory file + bug-locus disambiguation per Aaron's 'real
github bug?' question — answer: usage-bug, not tool-bug).

**Other substrate work:** #1399 BACKLOG.md regen, #1400 .ts/.sh
parity bug, #1402 assessment matrix doc update, #1405 B-0182
backlog row (Linux-only formal verification — orthogonal-axes
split per Aaron 2026-05-03).

**Discipline lessons captured:** chat-is-assertion-channel,
substrate-corrections-cluster, search-first-before-architectural-
expansion, verify-then-claim CI fidelity, documentation-is-
current-state-not-history.

Carved sentence: 'When a lucky catch surfaces a class of bug,
build the structural fix that eliminates the luck — audit + lint
gate + carved-sentence rule + memory file.'